A Proof of Weak Termination Providing the Right Way to Terminate
Identifieur interne : 006319 ( Main/Exploration ); précédent : 006318; suivant : 006320A Proof of Weak Termination Providing the Right Way to Terminate
Auteurs : Olivier Fissore [France] ; Isabelle Gnaedig [France] ; Hélène Kirchner [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract: We give an inductive method for proving weak innermost termination of rule-based programs, from which we automatically infer, for each successful proof, a finite strategy for data evaluation. We first present the proof principle, using an explicit induction on the termination property, to prove that any input data has at least one finite evaluation. For that, we observe proof trees built from the rewrite system, schematizing the innermost rewriting tree of any ground term, and generated with two mechanisms: abstraction, schematizing normalization of subterms, and narrowing, schematizing rewriting steps. Then, we show how, for any ground term, a normalizing rewriting strategy can be extracted from the proof trees, even if the ground term admits infinite rewriting derivations.
Url:
DOI: 10.1007/978-3-540-31862-0_26
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001024
- to stream Istex, to step Curation: 001008
- to stream Istex, to step Checkpoint: 001633
- to stream Main, to step Merge: 006544
- to stream PascalFrancis, to step Corpus: 000532
- to stream PascalFrancis, to step Curation: 000506
- to stream PascalFrancis, to step Checkpoint: 000527
- to stream Main, to step Merge: 006664
- to stream Main, to step Curation: 006319
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Proof of Weak Termination Providing the Right Way to Terminate</title><author><name sortKey="Fissore, Olivier" sort="Fissore, Olivier" uniqKey="Fissore O" first="Olivier" last="Fissore">Olivier Fissore</name></author><author><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:45082E71DD43AA1FF7687EA3A9164F37DB262653</idno><date when="2005" year="2005">2005</date><idno type="doi">10.1007/978-3-540-31862-0_26</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-75P5JMC3-B/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001024</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001024</idno><idno type="wicri:Area/Istex/Curation">001008</idno><idno type="wicri:Area/Istex/Checkpoint">001633</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001633</idno><idno type="wicri:doubleKey">0302-9743:2005:Fissore O:a:proof:of</idno><idno type="wicri:Area/Main/Merge">006544</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:05-0361907</idno><idno type="wicri:Area/PascalFrancis/Corpus">000532</idno><idno type="wicri:Area/PascalFrancis/Curation">000506</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000527</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000527</idno><idno type="wicri:doubleKey">0302-9743:2005:Fissore O:a:proof:of</idno><idno type="wicri:Area/Main/Merge">006664</idno><idno type="wicri:Area/Main/Curation">006319</idno><idno type="wicri:Area/Main/Exploration">006319</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Proof of Weak Termination Providing the Right Way to Terminate</title><author><name sortKey="Fissore, Olivier" sort="Fissore, Olivier" uniqKey="Fissore O" first="Olivier" last="Fissore">Olivier Fissore</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abstraction</term><term>Expert system</term><term>Induction</term><term>Knowledge base</term><term>Narrowing(logics)</term><term>Rewriting systems</term><term>Termination problem</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Abstraction</term><term>Base connaissance</term><term>Induction</term><term>Problème terminaison</term><term>Surréduction</term><term>Système expert</term><term>Système réécriture</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We give an inductive method for proving weak innermost termination of rule-based programs, from which we automatically infer, for each successful proof, a finite strategy for data evaluation. We first present the proof principle, using an explicit induction on the termination property, to prove that any input data has at least one finite evaluation. For that, we observe proof trees built from the rewrite system, schematizing the innermost rewriting tree of any ground term, and generated with two mechanisms: abstraction, schematizing normalization of subterms, and narrowing, schematizing rewriting steps. Then, we show how, for any ground term, a normalizing rewriting strategy can be extracted from the proof trees, even if the ground term admits infinite rewriting derivations.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Fissore, Olivier" sort="Fissore, Olivier" uniqKey="Fissore O" first="Olivier" last="Fissore">Olivier Fissore</name></noRegion><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006319 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006319 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:45082E71DD43AA1FF7687EA3A9164F37DB262653
|texte= A Proof of Weak Termination Providing the Right Way to Terminate
}}
| This area was generated with Dilib version V0.6.33. |  |